es:ES, i, x:Id, T:Type, P:(TProp), Lx:Knd List.
es-frame(es;i;Lx;x;T)
 e@i. (kind(e)  Lx)  P(x when e)  P((x after e))
 @i stable state.P(state.x)   

latex

Definitions	t  T, P  Q, x:A. B(x), x when e, (x after e), <a,b>, s = t, x(s), f(a), left+right, P  Q, Dec(P), e@i. P(e), {T}, SQType(T), Id, Prop, s ~ t, Atom$n, vartype(i;x), A/x,y. B(x;y), 1of(t), E, loc(e), x:AB(x), @i stable state.P(state)  , {x:A| B(x) }, x:AB(x), A & B, es-frame(es;i;L;x;T), ES, Type, type List, x. t(x), Knd, kind(e), (x  l)
Lemmas	alle-at wf, l member wf, es-frame wf, event system wf, es-after wf, es-loc wf, es-E wf, es-when wf, Id wf, Id sq, decidable l member, decidable equal Kind, es-kind wf, Knd wf